Nuprl Lemma : w-V_wf
0,22
postcript
pdf
the_w
:World,
i
:Id,
k
:Knd. V(
i
;
k
)
Type
latex
Definitions
World
,
V(
i
;
k
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
IdLnk
,
Knd
,
t
T
,
Id
Lemmas
Id
wf
,
Knd
wf
,
IdLnk
wf
,
kindcase
wf
,
world
wf
origin
the_w:World, i:Id, k:Knd. V(i;k) 
Type the_w:World, i:Id, k:Knd. V(i;k) Type 
x. t(x)x:A. B(x)x,y. t(x;y) T